This is gsumzsplit , gsumsplit , gsumsplit2 , gsummptfidmsplit ,
gsummptfidmsplitres , gsummptfzsplit , and gsummptfzsplitl

This is gsumconst from set.mm where the sum is indexed by consecutive
integers.  The proof is a new one by induction.

This is gsummhm from set.mm but where the sum is indexed by consecutive
integers.  The proof is from gsumfzval , seqhomog , and some monoid
theorems.

This is gsummhm2 from set.mm where the sum is indexed by
consecutive integers.  The proof is similar to the set.mm proof.

This is gsumconstf from set.mm but indexed by consecutive integers.  It
is also gsumfzconst from iset.mm but with a freeness hypothesis in place
of distinct variables.  The proof is similar to the set.mm proof of
gsumconstf .

This is gsumsnfd from set.mm except that M has to be an integer.
Naming this similarly to the other gsumfz* theorems seems more
appealing than trying to use a different convention.

The proof is similar to the set.mm proof.

Stated as in set.mm.  This is provided for compatibility with set.mm but
at least so far makes no effort to reduce axiom usage.  The proof is
based on the set.mm proof of cnfldadd .

This is gsumfsum from set.mm but where the sums are indexed by
consecutive integers.

As with the set.mm proof the proof separates the empty case (lemma
gsumfzfsumlem0 ) from the inhabited case (lemma gsumfzfsumlemm ,
here proved by induction which is perhaps simpler than trying to adapt
theorems like fsum3 ).

Stated as in set.mm.  The proof is the set.mm proof with one small
change in extensible structure theorems.

Stated as in set.mm.  At least for now, this uses the same complex
number axioms as cnfldmul .  The proof is from ax-mulf and cnfldmul .

This is similar to drngui from set.mm but for CCfld in particular, not
division rings in general.  The proof is a new one from crngunit ,
dvdsrd , and recapb .

This is expghm from set.mm with not equal changed to apart.  The proof
is basically the set.mm proof but needs changes of not equal to apart
and other intuitionizations on most steps.

Stated as in set.mm.  The proof is basically the set.mm proof but
requires intuitionizing in many places for a variety of reasons.
Remove one sentence from the comment in set.mm (which seemed to be an
incorrect copy-paste from lgseisenlem2 ).